i:Id, ds:fpf(Id; x.Type), da:fpf(Knd; k.Type), A:ecl(ds; da), snd:msg-spec(ds; da),
upd:update-spec(ds; da).
update-spec-decl(upd; ds)
 ((fpf-dom(id-deq; mkid{ecl:ut2}; ds)))
 fpf-compatible(Knd; k.Type; Kind-deq; R-da(ecl-machine{ecl:ut2}(i; ds; da; A; snd; upd); i); da
 fpf-compatible() 

latex

Definitions

sq_type(T), guard(T), fpf-compatible(A; a.B(a); eq; f; g), P  Q, T, x(s), P  Q, P  Q, ff, Y, tt, True, prop{i:l}, IdLnk, subtype(S; T), reduce(f; k; as), fpf-cap(f; eq; x; z), top, x. t(x), if b then t else f fi , ma-valtype(da; k), t  T, R-state-var-init(i; ds; da; x; T; v; ks; tr), ecl-machine3(ds; da; x; T; ks; a; snd), ecl-machine2(i; ds; da; x; T; ks; a; upd), spreadn(u; a,b,c,d,e,f,g.v(a;b;c;d;e;f;g)), ecl-machine1{$ecl:ut2}(i; ds; da; A), ecl-machine{$ecl:ut2}(i; ds; da; A; snd; upd), R-da(R; i), mkid{$x:ut2}, P  Q, Id, x:A. B(x), A c B, False, Unit, , ecl-trans-tuple{i:l}(ds; da), A,

Lemmas

IdLnk sq, lnk wf, lnk-decl-dom2, tagof wf, rcv wf, Knd sq, isrcv-implies, lnk-decl-dom-implies, es-dt-ap, lnk-decl-ap, R-lnk-tags-da, not functionality wrt iff, assert-eq-id, R-state-var-da, deq wf, true wf, squash wf, fpf-compatible wf, es-dt wf, lnk-decl wf, fpf-cap wf, lsrc wf, ifthenelse wf, ecl-tags wf, assert of bnot, eqff to assert, bnot wf, iff transitivity, fpf-ap wf, eqtt to assert, fpf-compatible-single-iff, fpf-compatible-symmetry, reduce wf, ma-valtype wf, fpf-single wf3, bool wf, eq id wf, Knd wf, fpf wf, ecl wf, msg-spec wf, update-spec wf, update-spec-decl wf, id-deq wf, Id wf, fpf-dom wf, assert wf, not wf, subtype rel list, msg-spec-links wf, idlnk-deq wf, IdLnk wf, remove-repeats wf, top wf, update-spec-vars wf, R-da-Rall, fpf-trivial-subtype-top, fpf-empty-compatible-left, ecl-machine3 wf, ecl-machine2 wf, fpf-empty wf, fpf-compatible-single, R-state-var wf, R-da wf, fpf-join wf, Kind-deq wf, fpf-compatible-join2, ecl-trans-tuple wf, ecl-trans wf